T:Type, L:(T List), R:({x:T| (x  L)} Realizer), B:Realizer.
R-icompat(B;xL.R(x))  (xL. R-icompat(B;R(x))) 

latex

Definitions	x. t(x), P  Q, P  Q, P & Q, xL. P(x), x(s), P  Q, t  T, x:A. B(x),
Lemmas	l all wf2, R-icompat wf, Rall wf, R-icompat symmetry, l member wf, es realizer wf, Rall-icompat